\documentclass[envcountsame]{llncs}

\usepackage[hmargin=1cm,vmargin=1cm]{geometry}

\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsfonts}
\usepackage{graphicx}
\usepackage{pdflscape}
%\usepackage{algorithm2e}
\usepackage{multicol}
\usepackage{subfig}
\usepackage{comment}


\usepackage{bussproofs}
\usepackage{proof}
\usepackage{url}

\usepackage{fancybox}
\usepackage{fancyvrb}

% Sequent Calculus Proof Settings
\EnableBpAbbreviations
\def\fCenter{\mbox{\ $\vdash$\ }}
\newcommand{\rl}[1]{\RightLabel{#1}}

\usepackage{commands}


\title{
  {\LJe} and \iCERes%
  %\thanks{}
}

\author{
  Alexander Leitsch%\inst{1}
  \and Giselle Reis%\inst{1}
  \and %\\
  Bruno Woltzenlogel Paleo%\inst{1}
}

\authorrunning{%D.\~Deharbe \and P.\~Fontaine \and S.\~Merz \and 
B.\~Woltzenlogel Paleo}

\institute{
  Theory and Logic Group, Institut f\"{u}r Computersprachen, Technische Universit\"{a}t Wien, Vienna, Austria \\
  \email{\{leitsch, giselle, bruno\}@logic.at}
}

% ===========================================================================


\newenvironment{calculus}{\begin{center}\begin{Sbox}\begin{minipage}{0.8\textwidth}}{\end{minipage}\end{Sbox}\fbox{\TheSbox}\end{center}}


% ===========================================================================

\begin{document}

\maketitle

\begin{abstract}

\end{abstract}



\section{\iCERes}

When {\CERes} is applied to a proof in {\LJe}, the resulting derivation is an {\LK}-proof but not an {\LJe}-proof. This unfortunate effect is shown in the example below.   

\begin{example}
Consider the proof $\varphi$ below:
\begin{prooftree}
\AXC{$P(a) \seq P(a)$} \RightLabel{$\ex_r$}
\UIC{$P(a) \seq \ex y. P(y)$}
		    \AXC{$P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$} \RightLabel{$\ex_r$}
		    \UIC{$P(\ep z. (Q\wedge P(z))  \ex y. P(y)$} \RightLabel{$w_l$}
		    \UIC{$Q, P(\ep z. (Q\wedge P(z)) \seq \ex y. P(y)$} \RightLabel{$\wedge_l$}
		    \UIC{$Q \wedge P(\ep z. (Q\wedge P(z)) \seq \ex y. P(y)$} \RightLabel{$\vee_l$}
	  \BIC{$P(a) \vee (Q \wedge P(\ep z. (Q\wedge P(z))) \seq \ex y. P(y)$}
			    \AXC{$P(\beta) \seq P(\beta)$} \RightLabel{$\neg_l$}
			    \UIC{$P(\beta), \neg P(\beta) \seq $} \RightLabel{$\all_l$}
			    \UIC{$P(\beta), \all u. \neg P(u) \seq $} \RightLabel{$\neg_r$}
			    \UIC{$P(\beta) \seq \neg \all u. \neg P(u)$} \RightLabel{$\ex_r$}
			    \UIC{$\ex y. P(y) \seq \neg \all u. \neg P(u)$} \RightLabel{$cut$}
		\BIC{$P(a) \vee (Q \wedge P(\ep z. (Q\wedge P(z))) \seq \neg \all u. \neg P(u)$}  
\end{prooftree}

Its clause set $\clauseset{\varphi}$ is:
$$
\{
\seq P(a), P(\ep z. (Q\wedge P(z)) \ \ ; \ \
P(\beta) \seq
\}
$$

It can be refuted by the following resolution refutation $\delta$:
\begin{prooftree}
\AXC{$\seq P(a), P(\ep z. (Q\wedge P(z))$}
    \AXC{$P(\beta) \seq$}
  \BIC{$\seq P(a)$}
	\AXC{$P(\beta) \seq$}
      \BIC{$\seq$}
\end{prooftree}

The projections are:

\begin{prooftree}
\AXC{$P(a) \seq P(a)$} 
		    \AXC{$P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$}  \RightLabel{$w_l$}
		    \UIC{$Q, P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$} \RightLabel{$\wedge_l$}
		    \UIC{$Q \wedge P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$} \RightLabel{$\vee_l$}
	  \BIC{$P(a) \vee (Q \wedge P(\ep z. (Q\wedge P(z))) \seq P(a), P(\ep z. (Q\wedge P(z))$}
\end{prooftree}

\begin{prooftree}
			    \AXC{$P(\beta) \seq P(\beta)$} \RightLabel{$\neg_l$}
			    \UIC{$P(\beta), \neg P(\beta) \seq $} \RightLabel{$\all_l$}
			    \UIC{$P(\beta), \all u. \neg P(u) \seq $} \RightLabel{$\neg_r$}
			    \UIC{$P(\beta) \seq \neg \all u. \neg P(u)$}
\end{prooftree}

The ACNF is:

\begin{tiny}
\begin{prooftree}
\AXC{$P(a) \seq P(a)$} 
		    \AXC{$P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$}  \RightLabel{$w_l$}
		    \UIC{$Q, P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$} \RightLabel{$\wedge_l$}
		    \UIC{$Q \wedge P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$} \RightLabel{$\vee_l$}
	  \BIC{$P(a) \vee (Q \wedge P(\ep z. (Q\wedge P(z))) \seq P(a), P(\ep z. (Q\wedge P(z))$}
			    \AXC{$P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$} \RightLabel{$\neg_l$}
			    \UIC{$P(\ep z. (Q\wedge P(z)), \neg P(\ep z. (Q\wedge P(z)) \seq $} \RightLabel{$\all_l$}
			    \UIC{$P(\ep z. (Q\wedge P(z)), \all u. \neg P(u) \seq $} \RightLabel{$\neg_r$}
			    \UIC{$P(\ep z. (Q\wedge P(z)) \seq \neg \all u. \neg P(u)$} \RightLabel{$cut$}
		\BIC{$P(a) \vee (Q \wedge P(\ep z. (Q\wedge P(z))) \seq P(a), \neg \all u. \neg P(u)$}
				    \AXC{$P(a) \seq P(a)$} \RightLabel{$\neg_l$}
				    \UIC{$P(a), \neg P(a) \seq $} \RightLabel{$\all_l$}
				    \UIC{$P(a), \all u. \neg P(u) \seq $} \RightLabel{$\neg_r$}
				    \UIC{$P(a) \seq \neg \all u. \neg P(u)$} \RightLabel{$cut$}
      \BIC{$P(a) \vee (Q \wedge P(\ep z. (Q\wedge P(z))) \seq \neg \all u. \neg P(u)$}
\end{prooftree}
\end{tiny}
\end{example}

{\CERes} produces non-intuitionistic ACNFs because the clauses in the clause set
can contain more than one literal in the succedent and because the projections
can contain more than one literal in the succedents of their sequents. In this
document we investigate one way of adapting {\CERes} so that its ACNFs are
instuitionistic {\LJe}-proofs. Our approach is to remove the formulas from the 
right hand side of the sequent and add their negated forms to the left hand
side. Since clauses may now contain negated formulas, the resolution calculus
must also be adapted to resolve this kind of formulas.
%The most straightforward way of adapting {\CERes} so that its ACNFs are
%intuitionistic {\LJe}-proofs is to add disjunctions in the succedents of the
%clauses in the clause set and to add right disjunction rules to the projections
%when necessary. Since clauses may now contain disjunctive formulas, the
%resolution calculus must be adapted too. We must add disjunction rules to the
%resolution calculus, and we must allow resolution on non-atomic formulas too.

\begin{definition}[Intuitionistic Clause Set with Negations]
\label{def:ics}
 The \emph{intuitionistic characteristic clause set} is built analogously to the
 usual characteristic clause set, except that all the formulas on the right hand
 side are negated and added to the left hand side:

 \begin{itemize}
  \item If $\nu$ is an axiom, then $CL^{i}(\nu)$ is the sub-sequent composed only
  of the formulas that are cut-ancestors, such that all the formulas that would
  appear on the right-hand side are negated and added to the left-hand side.
  \item If $\nu$ is the result of the application of a unary rule on $\mu$, then
  $CL^{i}(\nu) = CL^{i}(\mu)$
  \item If $\nu$ is the result of the application of a binary rule on $\mu_1$
  and $\mu_2$, we have to distinguish two cases:
  \begin{itemize}
    \item If the rule is applied to ancestors of the cut formula, then $CL^{i}(\nu)
    = CL^{i}(\mu_1) \oplus CL^{i}(\mu_2)$.
    \item If the rule is not applied to ancestors of the cut formula, then
    $CL^{i}(\nu) = CL^{i}(\mu_1) \otimes CL^{i}(\mu_2)$.
  \end{itemize}
 \end{itemize}

% The \emph{intuitionistic characteristic clause set} is built analogously to
% the usual characteristic clause set, but all literals that would appear in the
% right side are negated and added to the left side instead.
\end{definition}

Note that since the formulas on the right hand side are moved to the left hand
side already on the axioms, the clauses always have the right side empty. This
guarantees that we always have intuitionistic sequents and no conflicts arrise
while merging. 

\begin{theorem}[Unsatisfiability of the Intuitionistic Clause Set]
The intuitionistic clause set with negations is unsatisfiable. 
\end{theorem}
\begin{proof}
 Let $\varphi$ be an LJ proof and $CL^{i}(\varphi)$ be its intuitionistic clause
 set built according to Definition \ref{def:ics} and $CL(\varphi)$ be its
 classical clause set obtained on the classical version of CERES \cite{put
 reference}. For each clause $C_i = A_1, ..., A_n \vdash B_1, ..., B_m$ of the
 classical clause set, we build the closed formula $F_i = \forall \overline{x}.
 \neg (A_1 \wedge ... \wedge A_n \wedge \neg B_1 \wedge ... \wedge \neg B_m)$.

 By previous results, we know that there is an LK refutation $\psi$ of
 $CL(\varphi)$:
 
 \[
  \infer[]{\vdash}
  {
    \infer[]{\vdots}{C_1}
    &
    ...
    &
    \infer[]{\vdots}{C_k}
  }
 \]

 By merging each formula $F_i$ to its corresponding clause $C_i$
 and propagating it down the refutation, we obtain an LK proof $\psi_1$ from the
 axioms $F_i, A_1, ..., A_n \vdash B_1, ..., B_m$ (which are obviously provable
 in LK) of the end-sequent $F_1, ..., F_k \vdash$:
 
 \[
  \infer[]{F_1, ..., F_k \vdash}
  {
    \infer[]{\vdots}{F_1 \circ C_1}
    &
    ...
    &
    \infer[]{\vdots}{F_k \circ C_k}
  }
 \]

 We can transform the proof $\psi_1$ into a proof $\psi_2$ of $\vdash \neg (F_1
 \wedge ... \wedge F_k)$:

 \[
  \infer[\neg_r]{\vdash \neg (F_1 \wedge ... \wedge F_k)}
  {
    \infer=[\wedge_l \times (k-1)]{F_1 \wedge ... \wedge F_k \vdash}
    {
      \infer[]{F_1, ..., F_k \vdash}{\psi_1}
    }
  }
 \]

  Since the axioms of this proof are tautological, we can transform this into an
  LJ proof $\psi_3$ via negative translation. The end-sequent of $\psi_3$ is
  $\vdash \neg (\tilde{F}_1 \wedge ... \wedge \tilde{F}_k)$, where each
  $\tilde{F}_i$ is the negative translation of $F_i$. Note that $\vdash \neg
  \neg \neg A$ is LJ-equivalent to $\vdash \neg A$, so there is still only one
  negation on this end-sequent.

  From the proof $\psi_3$, we can construct the proof $\psi_4$:

  \[
    \infer[cut]{\vdash}
    {
      \infer[]{\vdash \neg (\tilde{F}_1 \wedge ... \wedge \tilde{F}_k)}{\psi_3}
      &
      \infer[\neg_l]{\neg (\tilde{F}_1 \wedge ... \wedge \tilde{F}_k) \vdash}
      {
        \infer=[\wedge_r \times k]{\vdash \tilde{F}_1 \wedge ... \wedge \tilde{F}_k}
        {
          \vdash \tilde{F}_1
          &
          ...
          &
          \vdash \tilde{F}_k
        }
      }
    }
  \]

  Note that the leaves of the right branch of $\psi_4$ are all of the form:

  $$\vdash \neg \neg \forall x_1. ... \neg \neg \forall x_r. \neg \neg \neg (A_1
  \wedge ... \wedge A_n \wedge \neg B_1 \wedge ... \wedge \neg B_m)$$

  We can apply the following backward derivation in each of these sequents:

  \[
    \infer=[\neg_r, \neg_l, \forall_r]{\vdash \neg \neg \forall x_1. ... \neg
    \neg \forall x_r. \neg \neg \neg (A_1
  \wedge ... \wedge A_n \wedge \neg B_1 \wedge ... \wedge \neg B_m)}
    {
      \infer=[\neg_r, \neg_l, \forall_r]{\vdash \neg \neg \forall x_2. ... \neg
      \neg \forall x_r. \neg \neg \neg (A_1
      \wedge ... \wedge A_n \wedge \neg B_1 \wedge ... \wedge \neg B_m)}
      {
        \infer[]{\vdots}
        {
          \infer=[\neg_r, \neg_l, \neg_r]{\vdash \neg \neg \neg (A_1 \wedge ... \wedge A_n \wedge \neg B_1 \wedge ... \wedge \neg B_m)}
          {
            \infer=[\wedge_l \times (n+m-1)]{A_1 \wedge ... \wedge A_n \wedge \neg B_1 \wedge ... \wedge
            \neg B_m \vdash }
            {A_1, ..., A_n, \neg B_1, ..., \neg B_m \vdash }
          }
        }
      }
    }
  \]

  So, we obtain an LK refutation of the clauses $A_1, ..., A_n, \neg B_1, ...,
  \neg B_m \vdash$, which are exactly the elements of $CL^{i}(\varphi)$. We
  conclude that this clause set is unsatisfiable.

\end{proof}



\begin{definition}[Intuitionistic Projection]
 An \emph{intuitionistic projection} is built analogously to a usual projection. However, during proof-recursive construction, whenever two branches having different succedent formulas in their end-sequents need to be combined via a non-cut-pertinent inference, we must first perform $\neg_l$ inferences in the bottom of each branch. 
\end{definition}

\begin{definition}
 The {\Rneg} calculus is the resolution calculus where the resolution rule is applied to negated formulas (i.e. it is a cut with unification restricted to formulas that are negated atoms) and the negation-right rule of {\LJe} is available. 
\end{definition}


\begin{example}
Consider the proof $\varphi$ below:
\begin{prooftree}
\AXC{$P(a) \seq P(a)$} \RightLabel{$\ex_r$}
\UIC{$P(a) \seq \ex y. P(y)$}
		    \AXC{$P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$} \RightLabel{$\ex_r$}
		    \UIC{$P(\ep z. (Q\wedge P(z))  \ex y. P(y)$} \RightLabel{$w_l$}
		    \UIC{$Q, P(\ep z. (Q\wedge P(z)) \seq \ex y. P(y)$} \RightLabel{$\wedge_l$}
		    \UIC{$Q \wedge P(\ep z. (Q\wedge P(z)) \seq \ex y. P(y)$} \RightLabel{$\vee_l$}
	  \BIC{$P(a) \vee (Q \wedge P(\ep z. (Q\wedge P(z))) \seq \ex y. P(y)$}
			    \AXC{$P(\beta) \seq P(\beta)$} \RightLabel{$\neg_l$}
			    \UIC{$P(\beta), \neg P(\beta) \seq $} \RightLabel{$\all_l$}
			    \UIC{$P(\beta), \all u. \neg P(u) \seq $} \RightLabel{$\neg_r$}
			    \UIC{$P(\beta) \seq \neg \all u. \neg P(u)$} \RightLabel{$\ex_r$}
			    \UIC{$\ex y. P(y) \seq \neg \all u. \neg P(u)$} \RightLabel{$cut$}
		\BIC{$P(a) \vee (Q \wedge P(\ep z. (Q\wedge P(z))) \seq \neg \all u. \neg P(u)$}  
\end{prooftree}

Its intuitionistic clause set $\clauseset{\varphi}$ is:
$$
\{
\neg P(a),  \neg P(\ep z. (Q\wedge P(z)) \seq \ \ ; \ \
P(\beta) \seq
\}
$$

It can be refuted by the following {\Rdisj}-refutation $\delta$:
\begin{prooftree}
\AXC{$P(\beta) \seq$} \RightLabel{$\neg_r$}
\UIC{$\seq \neg P(\beta)$}
    \AXC{$P(\gamma) \seq$} \RightLabel{$\neg_r$}
    \UIC{$\seq \neg P(\gamma)$}
	    \AXC{$\neg P(a),  \neg P(\ep z. (Q\wedge P(z)) \seq$}
	\BIC{$\neg P(\ep z. (Q\wedge P(z)) \seq$}
	\BIC{$\seq$}
\end{prooftree}

The projections are:

\begin{prooftree}
\AXC{$P(a) \seq P(a)$} \RightLabel{$\neg_l$}
\UIC{$P(a), \neg P(a) \seq$}
		    \AXC{$P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$}  \RightLabel{$w_l$}
		    \UIC{$Q, P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$} \RightLabel{$\wedge_l$}
		    \UIC{$Q \wedge P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$} \RightLabel{$\neg_l$}
		    \UIC{$Q \wedge P(\ep z. (Q\wedge P(z)), \neg P(\ep z. (Q\wedge P(z)) \seq $} \RightLabel{$\vee_l$}
	  \BIC{$P(a) \vee (Q \wedge P(\ep z. (Q\wedge P(z))), \neg P(a), \neg P(\ep z. (Q\wedge P(z)) \seq $}
\end{prooftree}

\begin{prooftree}
			    \AXC{$P(\beta) \seq P(\beta)$} \RightLabel{$\neg_l$}
			    \UIC{$P(\beta), \neg P(\beta) \seq $} \RightLabel{$\all_l$}
			    \UIC{$P(\beta), \all u. \neg P(u) \seq $} \RightLabel{$\neg_r$}
			    \UIC{$P(\beta) \seq \neg \all u. \neg P(u)$}
\end{prooftree}

The output proof is:

\begin{tiny}
\begin{prooftree}
\AXC{$P(a) \seq P(a)$} \RightLabel{$\neg_l$}
\UIC{$P(a), \neg P(a) \seq $} \RightLabel{$\all_l$}
\UIC{$P(a), \all u. \neg P(u) \seq $} \RightLabel{$\neg_r$}
\UIC{$P(a) \seq \neg \all u. \neg P(u)$}  \RightLabel{$\neg_r$}
\UIC{$\seq \neg \all u. \neg P(u), \neg P(a)$} 
	\AXC{$P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$} \RightLabel{$\neg_l$}
	\UIC{$P(\ep z. (Q\wedge P(z)), \neg P(\ep z. (Q\wedge P(z)) \seq $} \RightLabel{$\all_l$}
	\UIC{$P(\ep z. (Q\wedge P(z)), \all u. \neg P(u) \seq $} \RightLabel{$\neg_r$}
	\UIC{$P(\ep z. (Q\wedge P(z)) \seq \neg \all u. \neg P(u)$}  \RightLabel{$\neg_r$}
	\UIC{$ \seq \neg \all u. \neg P(u), \neg P(\ep z. (Q\wedge P(z))$}
		\AXC{$P(a) \seq P(a)$} \RightLabel{$\neg_l$}
		\UIC{$P(a), \neg P(a) \seq$}
		      \AXC{$P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$}  \RightLabel{$w_l$}
		      \UIC{$Q, P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$} \RightLabel{$\wedge_l$}
		      \UIC{$Q \wedge P(\ep z. (Q\wedge P(z)) \seq P(\ep z. (Q\wedge P(z))$} \RightLabel{$\neg_l$}
		      \UIC{$Q \wedge P(\ep z. (Q\wedge P(z)), \neg P(\ep z. (Q\wedge P(z)) \seq $} \RightLabel{$\vee_l$}
		   \BIC{$P(a) \vee (Q \wedge P(\ep z. (Q\wedge P(z))), \neg P(a), \neg P(\ep z. (Q\wedge P(z)) \seq $} \RightLabel{$cut$}
	    \BIC{$\neg P(a), P(a) \vee (Q \wedge P(\ep z. (Q\wedge P(z))) \seq \neg \all u. \neg P(u)$} \RightLabel{$cut$}
      \BIC{$P(a) \vee (Q \wedge P(\ep z. (Q\wedge P(z))) \seq \neg \all u. \neg P(u)$}
\end{prooftree}
\end{tiny}

Just for comparison, this is the cut-free proof obtained by reductive methods:

\begin{prooftree}
\AXC{$P(a) \seq P(a)$} \RightLabel{$ \neg_l $}
\UIC{$P(a), \neg P(a) \seq $} \RightLabel{$ \all_l $}
\UIC{$P(a), \all y. \neg P(y) \seq $} \RightLabel{$ \neg_r $}
\UIC{$P(a) \seq \neg \all y. \neg P(y)$}
		    \AXC{$P(\alpha) \seq P(\alpha)$} \RightLabel{$ \neg_l $}
		    \UIC{$P(\alpha), \neg P(\alpha) \seq $} \RightLabel{$ \all_l $}
		    \UIC{$P(\alpha), \all y. \neg P(y) \seq $} \RightLabel{$ \neg_r $}
		    \UIC{$P(\alpha) \seq \neg \all y. \neg P(y)$} \RightLabel{$ w_l $}
		    \UIC{$Q, P(\alpha) \seq \neg \all y. \neg P(y)$} \RightLabel{$ \wedge_l $}
		    \UIC{$Q \wedge P(\alpha) \seq \neg \all y. \neg P(y)$} \RightLabel{$ \ex_l $}
		    \UIC{$\ex z. (Q \wedge P(z)) \seq \neg \all y. \neg P(y)$} \RightLabel{$ \vee_l $}
	  \BIC{$P(a) \vee \ex z. (Q \wedge P(z)) \seq \neg \all y. \neg P(y)$}
\end{prooftree}
\end{example}




\vspace{-10pt}
\bibliographystyle{plain}
\bibliography{Bibliography}

\end{document}
